My friend Benja Fallenstein got carried away
in the comment section of my latest post on recursion and wrote a tutorial on how it all relates to denotational semantics. It’s a shame it is buried somewhere in the comments, so I am reposting the comment here with Benja’s permission.
The tagline is,
Denotational semantics tutorials. It s the new monad tutorials!
Benja Fallenstein writes:
Having read and understood
[the] entire post, I can now summarize Antti-Juhani s complaint in a way that programmers with no theoretical background will understand:
The definition is an infinite recursion. Sure, it s self-referential, but since it recurses forever, it doesn t actually define what recursion is!
:-)
That said, I find it kind of a pity to introduce all this theory without talking about why it nicely models the real world. Antti-Juhani argues that this pretty much the definition of popularized science, but I have to admit that, as definitions go, I like recursion: see recursion better.
So let me have a quick go. [UPDATE: Didn t turn out to be quick at all. This is, in fact, as long as Antti-Juhani s original post. Proceed at your own peril.]
All of this comes from denotational semantics, which is concerned with what expressions in a programming language mean and which ones mean the same thing. For example, 7 denotes the number seven, 7+2 denotes the number nine, and 5+4 also denotes the number nine.
Now, here s the knotty problem. If we have
f(x) = if x = 0 then 1 else x*f(x-1)
then f(4) denotes the number twenty-four, but what does f(-2) denote?
So, denotational semantics introduces a new, special value, recurses forever. An expression of type integer either denotes an integer, or, like f(-2), it denotes recurses forever.
Now, about these partial orders. (Reminder: A partial order says, for every pair (x,y) of elements of a certain set, that x is smaller than y, equal to y, larger than y, or incomparable to y.) Here is Benja s guide to what the partial orders of denotational semantics mean:
Let s say that you write a program where, in one place, you can plug in either x or y. If you can write such a program that prints foo when you plug in x and prints bar when plug in y, then x and y are incomparable. If you can t do that, but you can write a program that prints foo when you plug in y, and recurses forever when you plug in x, then x is smaller than y. If every program you can write will do the same thing whether you plug in x or y, then x and y are equal.
(We ignore details like out-of-memory errors and *how long* a program takes to do something.)
Examples:
- 5 and 7 are incomparable. Proof: if ___ == 5 then print foo else print bar .
- f(-2) f(2). Proof: if ___ == 2 then print foo else print foo if you plug in f(-2), this will loop forever, if you plug in f(2), it ll print foo .
- (5+2) = 7. Whatever program I write, it will do the same thing, no matter which of these expressions I plug in.
Now, with expressions of type integer, the resulting partial order is: Recurses forever is smaller than everything else. All other values are incomparable.
Recall from Antti-Juhani s post that the bottom element ( ) is defined to be the smallest element of a mathematical universe (if such a beast exists). Since recurses forever is smaller than everything else, it s the bottom element of this universe. That s what denotational semantics calls it. (Haskell, too.)
Of course, this partial order is kind of boring (the technical term is flat ). It gets more interesting when we consider functions.
In general, we can talk about functions from values of type S to values of type T, where we already know the partial orders of S and T. In particular, we can talk about functions from integers to integers.
Now, if you can find an x and a program that prints foo when you plug in f(x) and bar if you plug in g(x), then you can write a program that prints foo when you plug in f, and bar when you plug in g. (Exercise!
) Further, denotational semantics wants applying a function to a parameter and then doing something with the result to be the *only* way you can get information about a function. No f.get_function_name, please. (If your programming language has that, you can t map the functions of your programming language 1:1 to the functions of denotational semantics.)
By my rule above, this implies that f = g if and only if f(x) = g(x) for all x. Since formal theories can t have fuzzy stuff like my rule, denotational semantics takes this as the *definition* of the partial order on functions.
The bottom element of this mathematical universe, then, is the function that always returns bottom, no matter what it is given or in other words, a function that recurses forever, no matter what parameter you pass to it.
(Side note. Denotational semantics allows only monotone functions that is, if x = y, then f(x) = f(y) for all f, x, and y. That s an example of how all these definitions allow us to make formal statements about the real world. In the real world, if you can find a function f and a program that prints foo when given f(x) and bar when given f(y), then you have a program that prints foo when given x and bar when given y so if f(x) and f(y) are incomparable, then x and y must be incomparable, and the other way around, if x and y are comparable, then f(x) and f(y) must be comparable, too. (This reasoning doesn t exclude the case that x = y and f(x) >= f(y). If you really care, prove it yourself.
) This ends the side note.)
Recall, now, Antti-Juhani s definition of recursion: An equation of the form x = some expression (which may contain x), interpreted as a recursive definition, defines x to be the smallest value satisfying this equation. The models constructed in denotational semantics have the property that for any equation of this form, the set of values satisfying it does have a smallest element, so x is well-defined no matter what the equation is.
It s important to note that this does not mean that x has to be bottom, because there are equations to which bottom is not a solution. Let s look at a slightly simpler example than the one Antti-Juhani gave.
f(x) = if x = 0 then 0 else f(x-1)
We have f(0) = 1, but bottom(0) = bottom, so f can t be bottom.
The equation has more than one solution, though. It is satisfied by a function that returns 0 for x >= 0 and returns bottom (recurses forever) for x 0; but it is also satisfied by a function that returns 0 for every input. And by an infinite number of functions that return 0 for some negative inputs and bottom for others.
We want the first of these solutions, of course, because that s what we get if we interpret the equation as a computer program, and computer programs are what we re trying to model. But we re in luck: The first solution is smaller than all the other ones, because for all inputs, they either return the same value, or the solution we want returns bottom and the solution we don t want returns 0 (and bottom 0).
The point of it all is, of course, that when we interpret an equation as a computer program, we always get the least value satisfying the equation (if we use a partial order that follows my rule, above). And that, my friend, is denotational semantics.
I'm pondering adding more RAM to
my workstation. 128Mb is enough for most
of my work, but OpenOffice swaps a lot.
I couldn't remember what RAM is currently
in it (one stick or two?) so I was very
happy to find
dmidecode
in the comments on
as days pass by, by Stuart Langridge: Memory scanner for Linux.
dmidecode says I
have a free slot and
another 512Mb stick is surprisingly cheap.
Actually,
whole Ubuntu-ready-to-use computers are surprisingly cheap, according to lkcl.
I hope they don't contain
toxic e-waste.
I must be getting old. [Antti-Juhani Kaijanaho]
I was born on the 2nd of November in the year 1977, thirty years ago today, at 20:18 +0200.
Argh.
I’m scared.
Does it always feel like you’re about to die? 